Section: New Results

Bounding message length in attacks against security protocols

Participant : Marie Duflot-Kremer.

Security protocols are short programs that describe communication between two or more parties in order to achieve security goals. Despite the apparent simplicity of such protocols, their verification is a difficult problem and has been shown to be undecidable in general. This undecidability comes from the fact that the set of executions to be considered is of infinite depth (an infinite number of protocol sessions can be run) and infinitely branching (the intruder can generate an unbounded number of distinct messages). Several attempts have been made to tackle each of these sources of undecidability. Together with Myrto Arapinis, we have shown [22] that, under a syntactic and reasonable condition of “well-formedness” on the protocol, we can get rid of the infinitely branching part. More precisely we proved that as far as the secrecy property is considered and for a well-formed protocol, we just need to consider well-typed attacks, with a strong typing system. This result directly implies that the messages to be considered are of bounded length. We are currently working on a journal version of this result that extends the set of security properties to which the result is applicable, in particular including authentication properties.